Pretty print havoc_object instructions
#6174
Conversation
SaswatPadhi
requested review from
kroening,
peterschrammel and
tautschnig
as code owners
|
cc: @feliperodri |
SaswatPadhi
force-pushed
the
havoc_object_as_string
branch
2 times, most recently
from
dbff795 to
892ff2c
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6174 +/- ##
===========================================
+ Coverage 75.30% 75.31% +0.01%
===========================================
Files 1450 1450
Lines 158480 158485 +5
===========================================
+ Hits 119348 119369 +21
+ Misses 39132 39116 -16
Continue to review full report at Codecov.
|
SaswatPadhi
added
aws
SaswatPadhi
force-pushed
the
havoc_object_as_string
branch
from
892ff2c to
c266846
Compare
| } | ||
| // fallthrough | ||
| } | ||
| // fallthrough |
There was a problem hiding this comment.
⛏️ 💡 might be more readable to just repeat the line from ASSIGN and break.
There was a problem hiding this comment.
You are right that having:
out << from_expr(ns, identifier, instruction.get_code()) << '\n';
break;in place of the two fallthrough comments above would probably be more explicit, but this would also lead to code duplication, so I am somewhat hesitant. I added the comments to make it explicit that we are going to fall into the next case.
Resolves #6125.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/My commit message includes data points confirming performance improvements (if claimed).White-space or formatting changes outside the feature-related changed lines are in commits of their own.